$\forall$$A$, $B$:Realizer.
\\[0ex]($\neg$($\uparrow$Rplus?($A$)))
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$Rplus?($B$)))
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$Rnone?($A$)))
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$Rnone?($B$)))
\\[0ex]$\Rightarrow$ ($\forall$$x$:MaName. $\neg$(($x$ $\in$ R{-}names($A$)) \& ($x$ $\in$ R{-}names($B$))))
\\[0ex]$\Rightarrow$ (R{-}loc($A$) = R{-}loc($B$) $\in$ Id)
\\[0ex]$\Rightarrow$ R{-}frame{-}compat($A$;$B$)